Recursion and induction are mature, well-understood topics in programming.
Yet their duals, co-recursion and co-induction, are still exotic and
underdeveloped programming features. We aim to put them on equal footing by
giving a foundation for co-recursion based on computation, analogous to the
original computational foundation of recursion. At the lower level, we show
how the connection between the two can be strengthened through their
implementation details in an abstract machine. At the higher level, we
develop a syntactic equational theory for inductive and co-inductive
reasoning based on control flow. We also observe the impact of evaluation
strategy: call-by-name has efficient recursion and strong co-inductive
reasoning, but call-by-value has efficient co-recursion and strong inductive
reasoning.
more »
« less
Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher.
Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?
Some links on this page may take you to non-federal websites. Their policies may differ from this site.
-
-
A language supporting polymorphism is a boon to programmers: they can express complex ideas once and reuse functions in a variety of situations. However, polymorphism is a pain for compilers tasked with producing efficient code that manipulates concrete values. This paper presents a new intermediate language that allows for efficient static compilation, while still supporting flexible polymorphism. Specifically, it permits polymorphism over not only the types of values, but also the representation of values, the arity of primitive machine functions, and the evaluation order of arguments---all three of which are useful in practice. The key insight is to encode information about a value's calling convention in the kind of its type, rather than in the type itself.more » « less
-
The study of polarity in computation has revealed that an “ideal” programming language combines both call-by-value and call-by-name evaluation; the two calling conventions are each ideal for half the types in a programming language. But this binary choice leaves out call-by-need which is used in practice to implement lazy-by-default languages like Haskell. We show how the notion of polarity can be extended beyond the value/name dichotomy to include call-by-need by only adding a mechanism for sharing and the extra polarity shifts to connect them, which is enough to compile a Haskell-like functional language with user-defined types.more » « less
-
Modern programming languages have effects and mix multiple calling conventions, and their core calculi should too. We characterize calling conventions by their “substitution discipline” that says what variables stand for, and design calculi for mixing disciplines in a single program. Building on variations of the reducibility candidates method, including biorthogonality and symmetric candidates which are both specialized for one discipline, we develop a single uniform framework for strong normalization encompassing call-by-name, call-by-value, call-by-need, call-by-push-value, non-deterministic disciplines, and any others satisfying some simple criteria. We explicate commonalities of previous methods and show they are special cases of the uniform framework and they extend to multi-discipline programs.more » « less
Full Text Available